1  (isprop(p)∧(isprop(q)∧isprop(r)))⊃isprop(mkcond(p,q,r))   --- ∀E condsyn5 p,q,r

2  isprop(p)⊃iscond(mkcond(p,q,r))   --- ∀E condsyn0 p,q,r

3  isprop(mkcond(p,q,r))⊃iscond(mkcond(mkcond(p,q,r),a,b))   --- ∀E condsyn0 mkcond(p,q,r),a,b

4  isprop(p)⊃iscond(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))   --- ∀E condsyn0 p,mkcond(q,a,b),mkcond(r,a,b)

5  s1(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))=p   --- ∀E condsyn1 p,mkcond(q,a,b),mkcond(r,a,b)

6  s2(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))=mkcond(q,a,b)   --- ∀E condsyn2 p,mkcond(q,a,b),mkcond(r,a,b)

7  s3(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))=mkcond(r,a,b)   --- ∀E condsyn3 p,mkcond(q,a,b),mkcond(r,a,b)

8  s1(mkcond(p,q,r))=p   --- ∀E condsyn1 p,q,r

9  s2(mkcond(p,q,r))=q   --- ∀E condsyn2 p,q,r

10  s3(mkcond(p,q,r))=r   --- ∀E condsyn3 p,q,r

11  s1(mkcond(mkcond(p,q,r),a,b))=mkcond(p,q,r)   --- ∀E condsyn1 mkcond(p,q,r),a,b

12  (iscond(mkcond(p,q,r))∧value(s1(mkcond(p,q,r)))=T)⊃value(mkcond(p,q,r))=value(s2(mkcond(p,q,r)))   --- ∀E co~
ndval0 mkcond(p,q,r)

13  (iscond(mkcond(p,q,r))∧value(s1(mkcond(p,q,r)))=F)⊃value(mkcond(p,q,r))=value(s3(mkcond(p,q,r)))   --- ∀E co~
ndval1 mkcond(p,q,r)

14  (iscond(mkcond(p,q,r))∧value(s1(mkcond(p,q,r)))=U)⊃value(mkcond(p,q,r))=U   --- ∀E condval2 mkcond(p,q,r)

15  (iscond(mkcond(mkcond(p,q,r),a,b))∧value(s1(mkcond(mkcond(p,q,r),a,b)))=T)⊃value(mkcond(mkcond(p,q,r),a,b))=~
value(s2(mkcond(mkcond(p,q,r),a,b)))   --- ∀E condval0 mkcond(mkcond(p,q,r),a,b)

16  (iscond(mkcond(mkcond(p,q,r),a,b))∧value(s1(mkcond(mkcond(p,q,r),a,b)))=F)⊃value(mkcond(mkcond(p,q,r),a,b))=~
value(s3(mkcond(mkcond(p,q,r),a,b)))   --- ∀E condval1 mkcond(mkcond(p,q,r),a,b)

17  (iscond(mkcond(mkcond(p,q,r),a,b))∧value(s1(mkcond(mkcond(p,q,r),a,b)))=U)⊃value(mkcond(mkcond(p,q,r),a,b))=~
U   --- ∀E condval2 mkcond(mkcond(p,q,r),a,b)

18  (iscond(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))∧value(s1(mkcond(p,mkcond(q,a,b),mkcond(r,a,b))))=T)⊃value(mkc~
ond(p,mkcond(q,a,b),mkcond(r,a,b)))=value(s2(mkcond(p,mkcond(q,a,b),mkcond(r,a,b))))   --- ∀E condval0 mkcond(p,~
mkcond(q,a,b),mkcond(r,a,b))

19  (iscond(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))∧value(s1(mkcond(p,mkcond(q,a,b),mkcond(r,a,b))))=F)⊃value(mkc~
ond(p,mkcond(q,a,b),mkcond(r,a,b)))=value(s3(mkcond(p,mkcond(q,a,b),mkcond(r,a,b))))   --- ∀E condval1 mkcond(p,~
mkcond(q,a,b),mkcond(r,a,b))

20  (iscond(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))∧value(s1(mkcond(p,mkcond(q,a,b),mkcond(r,a,b))))=U)⊃value(mkc~
ond(p,mkcond(q,a,b),mkcond(r,a,b)))=U   --- ∀E condval2 mkcond(p,mkcond(q,a,b),mkcond(r,a,b))

21  isprop(p)⊃(value(p)=T∨(value(p)=F∨value(p)=U))   --- ∀E condtri1 p

22  (iscond(mkcond(p,q,r))∧value(p)=T)⊃value(mkcond(p,q,r))=value(s2(mkcond(p,q,r)))   --- SUBST 8 IN 12

23  (iscond(mkcond(p,q,r))∧value(p)=T)⊃value(mkcond(p,q,r))=value(q)   --- SUBST 9 IN 22

24  (iscond(mkcond(p,q,r))∧value(p)=F)⊃value(mkcond(p,q,r))=value(s3(mkcond(p,q,r)))   --- SUBST 8 IN 13

25  (iscond(mkcond(p,q,r))∧value(p)=F)⊃value(mkcond(p,q,r))=value(r)   --- SUBST 10 IN 24

26  (iscond(mkcond(p,q,r))∧value(p)=U)⊃value(mkcond(p,q,r))=U   --- SUBST 8 IN 14

27  (iscond(mkcond(mkcond(p,q,r),a,b))∧value(mkcond(p,q,r))=T)⊃value(mkcond(mkcond(p,q,r),a,b))=value(s2(mkcond(~
mkcond(p,q,r),a,b)))   --- SUBST 11 IN 15

28  s2(mkcond(mkcond(p,q,r),a,b))=a   --- ∀E condsyn2 mkcond(p,q,r),a,b

29  (iscond(mkcond(mkcond(p,q,r),a,b))∧value(mkcond(p,q,r))=T)⊃value(mkcond(mkcond(p,q,r),a,b))=value(a)   --- S~
UBST 28 IN 27

30  (iscond(mkcond(mkcond(p,q,r),a,b))∧value(mkcond(p,q,r))=F)⊃value(mkcond(mkcond(p,q,r),a,b))=value(s3(mkcond(~
mkcond(p,q,r),a,b)))   --- SUBST 11 IN 16

31  s3(mkcond(mkcond(p,q,r),a,b))=b   --- ∀E condsyn3 mkcond(p,q,r),a,b

32  (iscond(mkcond(mkcond(p,q,r),a,b))∧value(mkcond(p,q,r))=F)⊃value(mkcond(mkcond(p,q,r),a,b))=value(b)   --- S~
UBST 31 IN 30

33  (iscond(mkcond(mkcond(p,q,r),a,b))∧value(mkcond(p,q,r))=U)⊃value(mkcond(mkcond(p,q,r),a,b))=U   --- SUBST 11~
 IN 17

34  (iscond(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))∧value(p)=T)⊃value(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))=valu~
e(s2(mkcond(p,mkcond(q,a,b),mkcond(r,a,b))))   --- SUBST 5 IN 18

35  (iscond(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))∧value(p)=T)⊃value(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))=valu~
e(mkcond(q,a,b))   --- SUBST 6 IN 34

36  (iscond(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))∧value(p)=F)⊃value(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))=valu~
e(s3(mkcond(p,mkcond(q,a,b),mkcond(r,a,b))))   --- SUBST 5 IN 19

37  (iscond(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))∧value(p)=F)⊃value(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))=valu~
e(mkcond(r,a,b))   --- SUBST 7 IN 36

38  (iscond(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))∧value(p)=U)⊃value(mkcond(p,mkcond(q,a,b),mkcond(r,a,b)))=U   ~
--- SUBST 5 IN 20

39  isprop(q)⊃iscond(mkcond(q,a,b))   --- ∀E condsyn0 q,a,b

40  s1(mkcond(q,a,b))=q   --- ∀E condsyn1 q,a,b

41  s2(mkcond(q,a,b))=a   --- ∀E condsyn2 q,a,b

42  s3(mkcond(q,a,b))=b   --- ∀E condsyn3 q,a,b

43  isprop(r)⊃iscond(mkcond(r,a,b))   --- ∀E condsyn0 r,a,b

44  s1(mkcond(r,a,b))=r   --- ∀E condsyn1 r,a,b

45  s2(mkcond(r,a,b))=a   --- ∀E condsyn2 r,a,b

46  s3(mkcond(r,a,b))=b   --- ∀E condsyn3 r,a,b

47  (iscond(mkcond(q,a,b))∧value(s1(mkcond(q,a,b)))=T)⊃value(mkcond(q,a,b))=value(s2(mkcond(q,a,b)))   --- ∀E co~
ndval0 mkcond(q,a,b)

48  (iscond(mkcond(q,a,b))∧value(s1(mkcond(q,a,b)))=F)⊃value(mkcond(q,a,b))=value(s3(mkcond(q,a,b)))   --- ∀E co~
ndval1 mkcond(q,a,b)

49  (iscond(mkcond(q,a,b))∧value(s1(mkcond(q,a,b)))=U)⊃value(mkcond(q,a,b))=U   --- ∀E condval2 mkcond(q,a,b)

50  (iscond(mkcond(r,a,b))∧value(s1(mkcond(r,a,b)))=T)⊃value(mkcond(r,a,b))=value(s2(mkcond(r,a,b)))   --- ∀E co~
ndval0 mkcond(r,a,b)

51  (iscond(mkcond(r,a,b))∧value(s1(mkcond(r,a,b)))=F)⊃value(mkcond(r,a,b))=value(s3(mkcond(r,a,b)))   --- ∀E co~
ndval1 mkcond(r,a,b)

52  (iscond(mkcond(r,a,b))∧value(s1(mkcond(r,a,b)))=U)⊃value(mkcond(r,a,b))=U   --- ∀E condval2 mkcond(r,a,b)

53  (iscond(mkcond(q,a,b))∧value(s1(mkcond(q,a,b)))=T)⊃value(mkcond(q,a,b))=value(a)   --- SUBST 41 IN 47

54  (iscond(mkcond(q,a,b))∧value(q)=T)⊃value(mkcond(q,a,b))=value(a)   --- SUBST 40 IN 53

55  (iscond(mkcond(q,a,b))∧value(q)=F)⊃value(mkcond(q,a,b))=value(s3(mkcond(q,a,b)))   --- SUBST 40 IN 48

56  (iscond(mkcond(q,a,b))∧value(q)=F)⊃value(mkcond(q,a,b))=value(b)   --- SUBST 42 IN 55

57  (iscond(mkcond(q,a,b))∧value(q)=U)⊃value(mkcond(q,a,b))=U   --- SUBST 40 IN 49

58  (iscond(mkcond(r,a,b))∧value(r)=T)⊃value(mkcond(r,a,b))=value(s2(mkcond(r,a,b)))   --- SUBST 44 IN 50

59  (iscond(mkcond(r,a,b))∧value(r)=T)⊃value(mkcond(r,a,b))=value(a)   --- SUBST 45 IN 58

60  (iscond(mkcond(r,a,b))∧value(r)=F)⊃value(mkcond(r,a,b))=value(s3(mkcond(r,a,b)))   --- SUBST 44 IN 51

61  (iscond(mkcond(r,a,b))∧value(r)=F)⊃value(mkcond(r,a,b))=value(b)   --- SUBST 46 IN 60

62  (iscond(mkcond(r,a,b))∧value(r)=U)⊃value(mkcond(r,a,b))=U   --- SUBST 44 IN 52